\newcommand{\unf}[1]{\ensuremath{\mathbf{unfold}(#1)}}
\newcommand{\mcc}[1]{\ensuremath{\mathcal{#1}}}
\newcommand{\ty}{\ensuremath{T}}
\newcommand{\tyy}{\ensuremath{S}}
\newcommand{\bsub}{\ensuremath{\leq_{\mathtt{B}}}\xspace}
\newcommand{\csub}{\ensuremath{\leq_{\mathtt{C}}}\xspace}
\newcommand{\cdual}{\ensuremath{\,\bot_{\mathtt{C}}}\,}

This section discusses the extension of our approach 
with \emph{recursive types} and \emph{subtyping}.
These are two well-known ingredients of session type theories:
while recursion is present in early papers in binary session types~\cite{DBLP:conf/esop/HondaVK98},
subtyping was first studied by Gay and Hole in~\cite{DBLP:journals/acta/GayH05}.
Notice that 
by extending the types in Table~\ref{tab:types}  
with recursive types we obtain a type syntax that coincides with that in~\cite{DBLP:conf/esop/HondaVK98,DBLP:journals/entcs/YoshidaV07},
and is quite similar to that in~\cite{DBLP:journals/acta/GayH05}. 
As such, 
the incorporation of both recursive types  and subtyping closely follows prior works, 
and entails unsurprising technical details.
Still, the extension is interesting: on the one hand, recursive types increase the expressiveness of our language; on the other, 
subtyping allows us to refine the notion of interface (and interface ordering), thus enhancing our typed constructs for runtime adaptation.


\subsubsection{Extended Process and Type Syntax}\label{ss:extproc}
We begin by re-defining the process language. 
Consider an additional base set of \emph{recursion variables},
ranged over $\rv Y, \rv Y',\ldots$. 
In essence, we consider the language in 
Table~\ref{tab:syntax} without replicated session acceptance and with the addition of \emph{recursive calls}, denoted $\recu\,\rv Y. P$:
\begin{align*}
P, Q, R  ::= ~~ &   \nopenr{a}{x}.P   \sepr   \nopena{a}{x}.P \\
 \sepr &  \outC{k}{\tilde{e}}.P \sepr    \inC{k}{\tilde{x}}.P   
	  \sepr    \throw{k}{k'}.P \sepr    \catch{k}{x}.P   \\
	\sepr &  \select{k}{n};P \sepr   \branch{k}{n_1{:}P_1 \alte \cdots \alte n_m{:}P_m} \sepr \close{k}.P  \sepr   \restr{k}{P} \\
	\sepr &  \scomponent{l}{P}    	\sepr   \adapt{l}{P}{\mathsf{X}}  	     \sepr    \mathsf{X}  \sepr \recu\,\rv Y. P \sepr \rv Y \\
	\sepr &   P \para  P  \sepr   \ifte{e}{P}{Q} \sepr  \mathbf{0} 
 \end{align*}
Observe how a different font style distinguishes process variables (used in update processes)
from recursion variables. Notions of binding, $\alpha$-conversion, and substitution for recursion variables are completely standard;
 given a process $P$, we write 
  $\mathsf{frv}(P)$ and  $\mathsf{brv}(P)$ to denote its sets of  free/bound recursion variables.

 
The operational semantics for the modified language requires minor modifications.
Notions of structural congruence (Def.~\ref{d:strcong}), contexts (Def.~\ref{d:context}), and operations over contexts (Def.~\ref{d:opcontx})
are kept unchanged. The reduction semantics is the smallest relation on processes generated by 
the rules in Table~\ref{tab:semantics}, 
excepting rule $\rulename{r:ROPen}$ and adding the following additional rule:
$$
\begin{array}{ll}
 \rulename{r:Rec} &
C\{\recu\,\rv Y. P \} \pired C\{P\subst{\recu\,\rv Y. P }{\rv Y}\} 
\end{array}
$$



As for the type syntax, %We now develop required modifications in the type system.
the only addition are recursive types. 
Let us write $t, t', \ldots$ to denote recursive type variables.
The extended syntax for types is then as follows:
$$
\begin{array}{lclr}
\alpha, \beta &::=  & t & \text{type variable} \\ 
	      & \sepr &  \mu t.\alpha & \text{recursive type} \\ 	
	      & \sepr &  \cdots & \text{\{the other type constructs, as in Table \ref{tab:types} \}}	
\end{array}
$$

As customary, we adopt an \emph{equi-recursive} approach to recursive types, not distinguishing 
between $ \mu t.\alpha$ and its unfolding  $\alpha\subst{\mu t.\alpha}{t}$.
We restrict to \emph{contractive types}: a type is contractive if for each of its sub-expressions $\mu t.\mu t_1.\ldots.\mu t_n.\alpha$, the body $\alpha$ is not $t$.
Concerning typing environments,
we assume that recursion variables are included in the higher-order environment 
$\Theta$, thus extending the definition given in Table~\ref{tab:types} (lower part).
Finally, we shall require two typing rules for recursion variables and recursive calls; 
these are the first two rules in Table~\ref{tab:subt}.





\paragraph{An Example}
As a simple illustration,   consider a typical client/server scenario ($Client \para Server$) realized by the processes below:
 $$
\begin{array}{lcl}
 Server & := & \recu \, \rv Z. \nopena{a}{x}.(\rv Z \para \recu \, \rv Y.  \branch{x}{n_1{:}\inC{x}{v}.S_{\rv Y} \alte n_2{:}\close{x} } )\\
 S_{\rv Y}    & := & \nopenr{b}{z}.\outC{z}{v}.\inC{z}{r}.\close{z}.\outC{x}{r}.\rv Y \\
 Client & := & \nopenr{a}{x}. \select{x}{n_1}.\outC{x}{d_1}.\inC{x}{r}.\select{x}{n_1}.\outC{x}{d_2}.\inC{x}{r}.\select{x}{n_2}.\close{x}
\end{array}
$$
%\ref{ex:recclient}. 
We use recursion to implement (i) persistent services and (ii) services with recursive behaviors.   
Process $Server$ shows how to encode a behavior similar to $\repopen{a}{x}$: indeed once a session on $a$ is established a new copy of $Server$ is spawned. The body of the session has a recursive behavior: the client can choose between doing some computation on the server or closing the communication. If she chooses the first branch, then she sends some data to the server, the server processes them and sends back an answer $r$. At this point the client can choose again what to do: another computation or ending the session.

Processes $Server$ and $Client$ are well-typed under environments $\Gamma := v:\tau_1, r:\tau_2$ and $\Theta=\emptyset$. 
Indeed we can obtain the following type judgments:
$$
\begin{array}{ll}
 \judgebis{\env{\Gamma}{\Theta}}{Server}{\type{\emptyset}{ \quau \, a: \mu t. \&\{n_1{:}?({\capab_1}).!({\capab_2}).t, n_2{:}\epsilon \}, \quau \, b: \&\{n_1{:}!({\capab_1}).?({\capab_2}).\epsilon}}\\
 
 \judgebis{\env{\Gamma}{\Theta}}{Client}{\type{\emptyset}{ \INT}}\\
 
\end{array}
$$
where $\INT=\quau \, a: \oplus\{n_1{:}!({\capab_1}).?({\capab_2}).\oplus\{n_1{:}!({\capab_1}).?({\capab_2}). \oplus\{n_1{:}!({\capab_1}).?({\capab_2}).\epsilon, n_2{:}\epsilon \}, n_2{:}\epsilon \}, n_2{:}\epsilon \} $.
 
%\begin{table}[t!]
% 
% $$
%\begin{array}{lcl}
% Server & := & \recu \, \rv Z. \nopena{a}{x}.(\rv Z \para \recu \, \rv Y.  \branch{x}{n_1{:}\inC{x}{v}.S_{\rv Y} \alte n_2{:}\close{x} } )\\
% S_{\rv Y}    & := & \nopenr{b}{z}.\outC{z}{v}.\inC{z}{r}.\close{z}.\outC{x}{r}.\rv Y \\
% Client & := & \nopenr{a}{x}. \select{x}{n_1}.\outC{x}{d_1}.\inC{x}{r}.\select{x}{n_1}.\outC{x}{d_2}.\inC{x}{r}.\select{x}{n_2}.\close{x}
%\end{array}
%$$
% 
% 
%% $$
%% \begin{array}{lcl}
%%  Server & := & \recu \, \rv Z. \nopena{a}{x}.(\rv Z \para \outC{x}{1}.\inC{x}{y}.\recu \, \rv Y. \select{x}{y}. \branch{x}{1{:}\inC{x}{v}.S_{\rv Y}, 2{:}\close{x} } )\\
%% % S      & := & \outC{x}{1}.\inC{x}{y}.\recu \, Y. \select{x}{y}. \branch{x}{1{:}\inC{x}{v}.S_{\rv Y}, 2{:}\close{x} } \\
%%  S_{\rv Y}    & := & \nopenr{b}{z}.\outC{z}{v}.\inC{z}{r}.\close{z}.\outC{x}{r}.\inC{x}{y}.\outC{x}{y}.\rv Y \\
%%  Client & := & \nopenr{a}{x}.\inC{x}{y}.\outC{x}{1}. \recu \, \rv Y.\branch{x}{1{:}\select{x}{y}.C_{\rv Y} , 2{:}\select{x}{y}.\close{x}}\\
%% %            && \branch{x}{1{:}\select{x}{y}.C_{\rv Y} , 2{:}\select{x}{y}.\close{x}}\\
%%  C_{\rv Y}    & := & \outC{x}{d}.\inC{x}{r}.\ifte{\mathsf{ok}(r)}{\outC{x}{2}.\inC{x}{y}.Y}{\outC{x}{1}.\inC{x}{y}.\rv Y} 
%% \end{array}
%% $$
%\caption{Client/Server example}\label{ex:recclient}
%\end{table}




\subsubsection{Coinductive Subtyping and Duality}
We now introduce subtyping and duality, %essentially 
by adapting 
notions and definitions from~\cite{DBLP:journals/acta/GayH05}.
Intuitively, given session types $\alpha, \beta$, we shall say that 
$\alpha$ is a \emph{subtype} of $\beta$ %(noted $\alpha \subt \beta$) 
if %, 
%intuitively, 
any process of type $\alpha$ can safely be used in a context where a process of type $\beta$ is expected. 
More formally, let us write $\mathcal{T}$ to refer to the set of types, 
including both session types $\ST, \STT, \ldots$
and base types $\capab, \sigma, \ldots$.
We shall write 
$\ty, \tyy,  \ldots$ to range over $\mcc{T}$.
For all types, define $\unf{T}$ by recursion on the structure of $T$:
$\unf{\mu t.T} = \unf{T\subst{\mu t.T}{t}}$ and $\unf{T} = T$ otherwise.
Our definition of coinductive subtyping is given  next; it relies on 
 a subtyping relation \bsub over base types, which arises from subset relations 
(as in, e.g., $\mathsf{int} \bsub \mathsf{real}$).

%On basic types, subtyping arises from subset relations  $\mathsf{int} \subt \mathsf{real}$).
%For session types, $\subt$ is defined by the rules in Table~\ref{tab:subt}.



\begin{definition}
A relation $\mathcal{R} \subseteq \mathcal{T} \times \mathcal{T}$ is a \emph{type simulation}
if $(\ty, \tyy) \in \mathcal{R}$ implies the following conditions:
\begin{enumerate}[1.]
\item If $\unf{\ty} = \capab$ then $\unf{\tyy} = \sigma$ and $\capab \bsub \sigma$.

\item If $\unf{\ty} = \epsilon$ then $\unf{\tyy} = \epsilon$.

\item If $\unf{\ty} = ?(\ty_2).\ty_1$ then $\unf{\tyy} = ?(\tyy_2).\tyy_1$ and $(\ty_1, \tyy_1) \in \mcc{R}$ \\ and  $(\ty_2, \tyy_2)  \in \mcc{R}$.

\item If $\unf{\ty} = \,!(\ty_2).\ty_1$ then $\unf{\tyy} = \,!(\tyy_2).\tyy_1$ and $(\ty_1, \tyy_1) \in \mcc{R}$ \\ and  $(\tyy_2, \ty_2)  \in \mcc{R}$.

\item If $\unf{\ty} = ?(\tau_1, \ldots, \tau_n).\ty_1$ then $\unf{\tyy} = ?(\sigma_1, \ldots, \sigma_n).\tyy_1$ then
for all $i \in [1..n]$, we have that $(\tau_i, \sigma_i) \in \mcc{R}$ and $(\ty_1, \tyy_1) \in \mcc{R}$.

\item If $\unf{\ty} = !(\tau_1, \ldots, \tau_n).\ty_1$ then $\unf{\tyy} = !(\sigma_1, \ldots, \sigma_n).\tyy_1$ then
for all $i \in [1..n]$, we have that $(\sigma_i, \tau_i) \in \mcc{R}$ and $(\ty_1, \tyy_1) \in \mcc{R}$.

\item If $\unf{\ty} = \&\{n_1:\ty_1, \dots,  n_m:\ty_m \}$ then $\unf{\tyy} = \&\{n_1:\tyy_1, \dots,  n_h:\tyy_h \}$ 
and $m \leq h$
for all $i \in [1..m]$, we have that $(\ty_i, \tyy_i) \in \mcc{R}$.

\item If $\unf{\ty} = \oplus\{n_1:\ty_1, \dots,  n_m:\ty_m \}$ then $\unf{\tyy} = \oplus\{n_1:\tyy_1, \dots,  n_h:\tyy_h \}$ 
and $h \leq m$
for all $i \in [1..m]$, we have that $(\ty_i, \tyy_i) \in \mcc{R}$.

\end{enumerate}
\end{definition}

Observe how  $\subt$ is co-variant for input prefixes and contra-variant for outputs, 
whereas it is co-variant for branching and contra-variant for choices.
We have the following definition:


\begin{definition}
The coinductive subtyping relation, denoted \csub, is defined by $T \csub S$ if and only if there exists a type simulation $\mcc{R}$
such that $(T, S) \in \mcc{R}$.
\end{definition}

Following standard arguments (as in, e.g.,~\cite{DBLP:journals/acta/GayH05}), one may show:

\begin{lemma}
\csub is a preorder.
\end{lemma}

We now move on to define duality.
It is known that 
an inductive definition of duality (cf. Def.~\ref{d:dual})
is no longer appropriate
in the presence of recursive types  (see, e.g.,~\cite{DBLP:journals/entcs/VallecilloVR03}). 
This justifies the need for a 
\emph{coinductive} notion of  duality over session types; it is defined similarly as subtyping above.



\begin{definition}
A relation $\mathcal{R} \subseteq \mathcal{T} \times \mathcal{T}$ is a \emph{duality relation}
if $(\ty, \tyy) \in \mathcal{R}$ implies the following conditions:
\begin{enumerate}[1.]
\item If $\unf{\ty} = \capab$ then $\unf{\tyy} = \sigma$ and $\tau \csub \sigma$ and  $\sigma \csub  \tau$.

\item If $\unf{\ty} = \epsilon$ then $\unf{\tyy} = \epsilon$.

\item If $\unf{\ty} = ?(\ty_2).\ty_1$ then $\unf{\tyy} = !(\tyy_2).\tyy_1$ and $(\ty_1, \tyy_1) \in \mcc{R}$ \\ and  $\ty_2 \csub \tyy_2$ and $\tyy_2 \csub \ty_2$.

\item If $\unf{\ty} = \,!(\ty_2).\ty_1$ then $\unf{\tyy} = \,?(\tyy_2).\tyy_1$ and $(\ty_1, \tyy_1) \in \mcc{R}$ \\ and  $\ty_2 \csub \tyy_2$ and $\tyy_2 \csub \ty_2$.

\item If $\unf{\ty} = ?(\tau_1, \ldots, \tau_n).\ty_1$ then $\unf{\tyy} = ?(\sigma_1, \ldots, \sigma_n).\tyy_1$ then
for all $i \in [1..n]$, we have that $(\ty_1, \tyy_1) \in \mcc{R}$ and  $\tau_i \csub \sigma_i$ and  $\sigma_i \csub  \tau_i$.

\item If $\unf{\ty} = !(\tau_1, \ldots, \tau_n).\ty_1$ then $\unf{\tyy} = ?(\sigma_1, \ldots, \sigma_n).\tyy_1$ then
for all $i \in [1..n]$, we have that $(\ty_1, \tyy_1) \in \mcc{R}$ and  $\tau_i \csub \sigma_i$ and  $\sigma_i \csub  \tau_i$.

\item If $\unf{\ty} = \&\{n_1:\ty_1, \dots,  n_m:\ty_m \}$ then $\unf{\tyy} = \oplus\{n_1:\tyy_1, \dots,  n_m:\tyy_m \}$ and
for all $i \in [1..m]$, we have that $(\ty_i, \tyy_i) \in \mcc{R}$.

\item If $\unf{\ty} = \oplus\{n_1:\ty_1, \dots,  n_m:\ty_m \}$ then $\unf{\tyy} = \&\{n_1:\tyy_1, \dots,  n_m:\tyy_m \}$ and
for all $i \in [1..m]$, we have that $(\ty_i, \tyy_i) \in \mcc{R}$.

\end{enumerate}

\end{definition}

We may now define:

\begin{definition}
The coinductive duality relation, denoted \cdual, is defined by $T \cdual S$ if and only if there exists a duality relation $\mcc{R}$
such that $(T, S) \in \mcc{R}$. The extension of $\csub$ to typings and interfaces, written $\ActS \csub \ActS'$ and $\INT \csub \INT'$, respectively, 
arise as expected.
\end{definition}




%\subsection{Additional typing rules}


%definire = come antisimmetria
%da aggiungere a Def. 8
%Equality between interfaces $\INT_1 = \INT_2$ iff  $\INT_1 \intpr \INT_2$ and $\INT_2 \intpr \INT_1$


\begin{table}[t!]
$$
\begin{array}{c}
\infer[\rulename{t:RVar}]{\Gamma; \Theta,\rv Y: \ActS, \INT \vdash \rv Y:\type{\ActS}{\INT}}{}
\\ \\
\infer[\rulename{t:Rec} ]{\judgebis{\env{\Gamma}{\Theta}}{\recu\,\rv Y. P}{\type{\Delta}{\INT }}} 
{\judgebis{\env{\Gamma}{\Theta,\rv Y: \type{\ActS}{\INT}}}{P}{\type{\Delta}{ \INT}} }
\\ \\
\infer[\rulename{t:Subs} ]{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS'}{\INT'}} } 
{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\Delta}{ \INT}}& \ActS \csub \ActS' & \INT \csub \INT'}
\\
 \\
 \infer[\rulename{t:CResD}]{\judgebis{\env{\Gamma}{\Theta}} {\restr{\cha}{P}}{\type{\ActS, [\cha^-:\ST_1], [\cha^+:\ST_2]}{ \INT}}}
 {\judgebis{\env{\Gamma}{\Theta}}{P }{\type{\ActS, \cha^-:\ST_1, \cha^+:\ST_2 }{ \INT}} & \ST_1 \cdual \ST_2}
 \\
 \\
 \infer[\rulename{t:MonAdapt}]{\judgebis{\env{\Gamma}{\Theta}}{\adapt{l}{P}{\mathsf{X}}}{\type{\emptyset}{ \emptyset}}}{\Theta \vdash l:\INT_1  \qquad  \judgebis{\env{\Gamma}{\Theta,\mathsf{X}:{\INT_1}}}{P}{\type{\emptyset}{ \INT_2 }}  \qquad ~\INT_1 \intpr \INT_2~}  
\end{array}
$$
\caption{Well-typed processes with recursion and subtyping: New and/or modified rules } \label{tab:subt}
\end{table}

% where the operation $\mu t(\Delta)$ stands for the concurrent promotion of all typings in $\Delta$. More formally:
% $$
% \begin{array}{lcl}
%  \mu t(\emptyset)& =& \emptyset\\
%  \mu t(\Delta, k:ST) &=& \mu t(\Delta), k:\mu t. ST\\ 
%  \mu t(\Delta, [k:ST]) &=& \mu t(\Delta), [k:\mu t. ST] \text{HMMM non sono sicura controllare!}
%  \end{array}
% $$

%We may now redefine the notion of well-typedness for the 
%the process language introduced in this section:
%
%\begin{definition}%[Well-typed process]
%A process is well-typed if it can be typed using the rules in Tables~\ref{tab:ts} and~\ref{tab:session}.
%\end{definition}

\subsubsection{Refining Interfaces via Subtyping}
In most session type disciplines, the main use of duality typically arises in the rule for channel restriction;
similarly, the main use of (coinductive) subtyping is in the subsumption rule, 
which enables us to incorporate the flexibility of subtyping in derivations, increasing typability.
 Table~\ref{tab:subt} presents these rules for our framework, denoted~\rulename{t:CResD} and~\rulename{t:Subs}, respectively.
While the former represents the key duality check performed by the typing system, the latter 
covers both typing $\ActS$ and interface $\INT$. In the following we elaborate on another consequence of adding subtyping, namely its interplay with interface ordering (cf. Def~\ref{d:intpre}).

As argued along the paper, a main contribution of this work is the extension of session type disciplines with a simple notion of \emph{interface}.
Using interfaces, we are able to give
simple and intuitive typing rules for located and update processes---see rules \rulename{t:Loc} and \rulename{t:Adapt} in Table~\ref{tab:ts}.
It is thus legitimate to investigate how to 
enhance the notion of interface and its associated definitions.
In particular, we discuss an alternative based on subtyping.
%The discussion is kept brief and informal: our aim is to illustrate how the presented framework already provides
%a basis for more sophisticated analyses---a formal treatment of these ideas is out of the scope of this paper and is left for future work.
%A straightforward enhancement concerns the typing of adaptable processes. 
Consider rule~\rulename{t:MonAdapt} in Table~\ref{tab:subt}: it is intended as 
as alternative  formulation for typing rule~\rulename{t:Adapt} in Table~\ref{tab:ts}.
Although 
rule~\rulename{t:MonAdapt} is more restrictive than~\rulename{t:Adapt} (i.e., it accepts less update processes as typable),
it captures a requirement that may be desirable in several practical settings, namely that 
the behavior after adaptation is ``at least'' the behavior offered before, possibly adding new behaviors.
Indeed, by disallowing adaptation routines that discard behavior, rule \rulename{t:MonAdapt} is suitable 
to reason about settings in which adaptation/upgrade actions need to be tightly controlled. 

In the context of more stringent typing rules such as \rulename{t:MonAdapt}, it is convenient to find ways for adding flexibility to the 
interface preorder \intpr in Def.~\ref{d:intpre}. 
As this preorder is central to our approach for disciplined runtime adaptation, 
a relaxed definition for it
may  lead to more flexible typing disciplines.
One alternative is to rely on $\csub$
%\emph{subtyping} for session types 
for such a relaxed definition:
%We briefly recall the essential features of subtyping in session types; see~\cite{DBLP:journals/acta/GayH05,DBLP:journals/fuin/VallecilloVR06} for details. 
%By relying on $\subt$, it is possible to define a more flexible preorder over interfaces:

\begin{definition}[Refined Interface Preorder] \label{d:rintpre}Given interfaces $\INT$ and $\INT'$, we write 
$\INT  \intpr_\text{sub} \INT'$ iff 
\begin{enumerate}[1.]
\item $\forall (\qual\,a{:}\ST)$ such that  
 $\#_{\INT_\qual}(\qual\,a{:}\ST) = h$  with $h > 0$,
then  one of the following holds:
\begin{enumerate}[(a)]
\item there exists $h$ distinct elements $(\qual\,a{:}\STT_i) \in \INT'_\qual$ such that 
 $\ST \csub \STT_i$ for $ i \in [1..h]$;
\item there exists $(\quau\,a{:}\STT) \in \INT'_\quau$ such that  $\ST \csub \STT$.
\end{enumerate}
\item $\forall (\quau\,a{:}\ST) \in \INT_\quau $  then $ (\quau \, a{:}\STT) \in \INT'_\quau $ and $\ST \csub \STT$, for some $\STT$.
\end{enumerate}


\end{definition}


It is immediate to see how $\intpr_\text{sub}$ improves over $\intpr$ by 
offering a more flexible and fine-grained relation over interfaces, in which subtyping replaces strict type equality.

We are now finally ready to state the notion of well-typedness that concerns the processes introduced in this section:

\begin{definition}%[Well-typed process]
A (possibly recursive) process is well-typed if it can be typed using the rules in Table~\ref{tab:ts} (excepting \rulename{t:CRes} and \rulename{t:Adapt}), Table~\ref{tab:session}, and Table~\ref{tab:subt}.
\end{definition}

%Based on this definition of well-typed process, we may now state:
%As a consequence, 
We are confident 
that our main results (Theorems~\ref{th:subred},~\ref{t:safety}, and \ref{t:consist}) 
 also hold, with little modifications, for the enhanced framework 
that results from: (a)~replacing replication with recursion, using coinductive duality, 
and (b)~incorporating subtyping, also replacing \rulename{t:Adapt} with rule \rulename{t:MonAdapt} above, using $\intpr_\text{sub}$ in place of
\intpr  
in the appropriate places in Table~\ref{tab:ts}.
%Lemma~\ref{lem:substitution}(3), and Theorem~.

%Summing up, with the modifications detail in this sub-section
%
%\begin{claim}[Subject Reduction, Recursive Processes with Subtyping]\label{th:subred-sc}
%If $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}}$ with $\ActS$ balanced and $P \pired Q$ then 
% $\judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\ActS'}{\INT'}}$, for some $\INT'$ and balanced $\ActS'$.
%\end{claim}

%\begin{proof}[Proof (Sketch)]
%TBD.
%\end{proof}




%\subsection{Example}

